#ifndef _inline_h_INCLUDED
#define _inline_h_INCLUDED

#include "internal.h"
#include "logging.h"

#ifndef NMETRICS

static inline size_t
kissat_mab_allocated(kissat* solver)
{
	return solver->statistics.allocated_current;
}

#endif

static inline bool
kissat_mab_propagated(kissat* solver)
{
	return SIZE_STACK(solver->trail) == solver->propagated;
}

static inline value
kissat_mab_fixed(kissat* solver, unsigned lit)
{
	assert(lit < LITS);
	const value res = solver->values[lit];
	if (!res)
		return 0;
	if (LEVEL(lit))
		return 0;
	return res;
}

static inline void
kissat_mab_mark_removed_literal(kissat* solver, unsigned lit)
{
	const unsigned idx = IDX(lit);
	flags* flags = FLAGS(idx);
	if (flags->eliminate)
		return;
	LOG("marking variable %u removed", idx);
	flags->eliminate = true;
	INC(variables_removed);
}

static inline void
kissat_mab_mark_added_literal(kissat* solver, unsigned lit)
{
	const unsigned idx = IDX(lit);
	flags* flags = FLAGS(idx);
	if (flags->subsume)
		return;
	LOG("marking variable %u added", idx);
	flags->subsume = true;
	INC(variables_added);
}

static inline void
kissat_mab_push_large_watch(kissat* solver, watches* watches, reference ref)
{
	const watch watch = kissat_mab_large_watch(ref);
	PUSH_WATCHES(*watches, watch);
}

static inline void
kissat_mab_push_binary_watch(kissat* solver, watches* watches, bool redundant, bool hyper, unsigned other)
{
	const watch watch = kissat_mab_binary_watch(other, redundant, hyper);
	PUSH_WATCHES(*watches, watch);
}

static inline void
kissat_mab_push_blocking_watch(kissat* solver, watches* watches, unsigned blocking, reference ref)
{
	assert(solver->watching);
	const watch head = kissat_mab_blocking_watch(blocking);
	PUSH_WATCHES(*watches, head);
	const watch tail = kissat_mab_large_watch(ref);
	PUSH_WATCHES(*watches, tail);
}

static inline void
kissat_mab_watch_other(kissat* solver, bool redundant, bool hyper, unsigned lit, unsigned other)
{
	LOGBINARY(lit,
			  other,
			  "watching %s blocking %s in %s",
			  LOGLIT(lit),
			  LOGLIT(other),
			  (redundant ? "redundant" : "irredundant"));
	watches* watches = &WATCHES(lit);
	kissat_mab_push_binary_watch(solver, watches, redundant, hyper, other);
}

static inline void
kissat_mab_watch_binary(kissat* solver, bool redundant, bool hyper, unsigned a, unsigned b)
{
	kissat_mab_watch_other(solver, redundant, hyper, a, b);
	kissat_mab_watch_other(solver, redundant, hyper, b, a);
}

static inline void
kissat_mab_watch_blocking(kissat* solver, unsigned lit, unsigned blocking, reference ref)
{
	assert(solver->watching);
	LOGREF(ref, "watching %s blocking %s in", LOGLIT(lit), LOGLIT(blocking));
	watches* watches = &WATCHES(lit);
	kissat_mab_push_blocking_watch(solver, watches, blocking, ref);
}

static inline void
kissat_mab_unwatch_blocking(kissat* solver, unsigned lit, reference ref)
{
	assert(solver->watching);
	LOGREF(ref, "unwatching %s in", LOGLIT(lit));
	watches* watches = &WATCHES(lit);
	kissat_mab_remove_blocking_watch(solver, watches, ref);
}

static inline void
kissat_mab_disconnect_binary(kissat* solver, unsigned lit, unsigned other)
{
	assert(!solver->watching);
	watches* watches = &WATCHES(lit);
	const watch watch = kissat_mab_binary_watch(other, false, false);
	REMOVE_WATCHES(*watches, watch);
}

static inline void
kissat_mab_disconnect_reference(kissat* solver, unsigned lit, reference ref)
{
	assert(!solver->watching);
	LOGREF(ref, "disconnecting %s in", LOGLIT(lit));
	const watch watch = kissat_mab_large_watch(ref);
	watches* watches = &WATCHES(lit);
	REMOVE_WATCHES(*watches, watch);
}

static inline void
kissat_mab_watch_reference(kissat* solver, unsigned a, unsigned b, reference ref)
{
	assert(solver->watching);
	kissat_mab_watch_blocking(solver, a, b, ref);
	kissat_mab_watch_blocking(solver, b, a, ref);
}

static inline void
kissat_mab_connect_literal(kissat* solver, unsigned lit, reference ref)
{
	assert(!solver->watching);
	LOGREF(ref, "connecting %s in", LOGLIT(lit));
	watches* watches = &WATCHES(lit);
	kissat_mab_push_large_watch(solver, watches, ref);
}

static inline clause*
kissat_mab_unchecked_dereference_clause(kissat* solver, reference ref)
{
	return (clause*)&PEEK_STACK(solver->arena, ref);
}

static inline clause*
kissat_mab_dereference_clause(kissat* solver, reference ref)
{
	clause* res = kissat_mab_unchecked_dereference_clause(solver, ref);
	assert(kissat_mab_clause_in_arena(solver, res));
	return res;
}

static inline reference
kissat_mab_reference_clause(kissat* solver, const clause* c)
{
	assert(kissat_mab_clause_in_arena(solver, c));
	return (word*)c - BEGIN_STACK(solver->arena);
}

static inline void
kissat_mab_inlined_connect_clause(kissat* solver, watches* all_watches, clause* c, reference ref)
{
	assert(!solver->watching);
	assert(ref == kissat_mab_reference_clause(solver, c));
	assert(c == kissat_mab_dereference_clause(solver, ref));
	for (all_literals_in_clause(lit, c)) {
		assert(!solver->watching);
		LOGREF(ref, "connecting %s in", LOGLIT(lit));
		assert(lit < LITS);
		watches* lit_watches = all_watches + lit;
		kissat_mab_push_large_watch(solver, lit_watches, ref);
	}
}

static inline void
kissat_mab_watch_clause(kissat* solver, clause* c)
{
	assert(c->searched < c->size);
	const reference ref = kissat_mab_reference_clause(solver, c);
	kissat_mab_watch_reference(solver, c->lits[0], c->lits[1], ref);
}

static inline void
kissat_mab_update_queue(kissat* solver, const links* links, unsigned idx)
{
	assert(!DISCONNECTED(idx));
	const unsigned stamp = links[idx].stamp;
	LOG("queue updated to variable %u stamped %u", idx, stamp);
	solver->queue.search.idx = idx;
	solver->queue.search.stamp = stamp;
}

static inline int
kissat_mab_export_literal(kissat* solver, unsigned ilit)
{
	const unsigned iidx = IDX(ilit);
	assert(iidx < (unsigned)INT_MAX);
	int elit = PEEK_STACK(solver->exportk, iidx);
	if (!elit)
		return 0;
	if (NEGATED(ilit))
		elit = -elit;
	assert(VALID_EXTERNAL_LITERAL(elit));
	return elit;
}

static inline unsigned
kissat_mab_map_literal(kissat* solver, unsigned ilit, bool map)
{
	if (!map)
		return ilit;
	int elit = kissat_mab_export_literal(solver, ilit);
	if (!elit)
		return INVALID_LIT;
	const unsigned eidx = ABS(elit);
	const import* import = &PEEK_STACK(solver->import, eidx);
	if (import->eliminated)
		return INVALID_LIT;
	unsigned mlit = import->lit;
	if (elit < 0)
		mlit = NOT(mlit);
	return mlit;
}

static inline void
kissat_mab_update_variable_score(kissat* solver, heap* schedule, unsigned idx)
{
	assert(schedule->size);
	const unsigned lit = LIT(idx);
	const unsigned not_lit = NOT(lit);
	size_t pos = WATCHES(lit).size;
	size_t neg = WATCHES(not_lit).size;
	double new_score = ((double)pos) * neg + pos + neg;
	LOG("new elimination score %g for variable %u (pos %zu and neg %zu)", new_score, idx, pos, neg);
	kissat_mab_update_heap(solver, schedule, idx, -new_score);
}

static inline clause*
kissat_mab_last_irredundant_clause(kissat* solver)
{
	return (solver->last_irredundant == INVALID_REF) ? 0
													 : kissat_mab_dereference_clause(solver, solver->last_irredundant);
}

static inline clause*
kissat_mab_binary_conflict(kissat* solver, bool redundant, unsigned a, unsigned b)
{
	LOGBINARY(a, b, "conflicting");
	clause* res = &solver->conflict;
	res->redundant = redundant;
	res->size = 2;
	unsigned* lits = res->lits;
	lits[0] = a;
	lits[1] = b;
	return res;
}

static inline int
kissat_mab_checking(kissat* solver)
{
#ifndef NDEBUG
#ifdef NOPTIONS
	(void)solver;
#endif
	return GET_OPTION(check);
#else
	(void)solver;
	return 0;
#endif
}

static inline bool
kissat_mab_logging(kissat* solver)
{
#ifdef LOGGING
#ifdef NOPTIONS
	(void)solver;
#endif
	return GET_OPTION(log) > 0;
#else
	(void)solver;
	return false;
#endif
}

static inline bool
kissat_mab_proving(kissat* solver)
{
#ifdef NPROOFS
	(void)solver;
	return false;
#else
	return solver->proof != 0;
#endif
}

static inline bool
kissat_mab_checking_or_proving(kissat* solver)
{
	return kissat_mab_checking(solver) || kissat_mab_proving(solver);
}

#if !defined(NDEBUG) || !defined(NPROOFS)
#define CHECKING_OR_PROVING
#endif

#endif
